InforLorV4, Main, Exploration, bibRecord, 002802

Sequent calculi and decidability for intuitionistic hybrid logic

Identifieur interne : 002802 ( Main/Exploration ); précédent : 002801; suivant : 002803

Sequent calculi and decidability for intuitionistic hybrid logic

Auteurs : Didier Galmiche [France] ; Yakoub Salhi [France]

Source :

Information and computation : (Print) [ 0890-5401 ] ; 2011.

RBID : Pascal:12-0044340

Descripteurs français

Pascal (Inist)
- Informatique théorique, Décidabilité, Logique intuitionniste, Théorie preuve, Théorie constructive, Calcul séquent, Consistance sémantique, Complétude, Elimination coupure, 03B20, 03Fxx, 68T15, Déduction naturelle, Procédure décision.

English descriptors

KwdEn :
- Completeness, Computer theory, Constructive theory, Cut elimination, Decidability, Intuitionistic logic, Proof theory, Sequent calculus, Soundness.

Abstract

In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for _IHL and then prove its decidabilit^y.

Url:

https://hal.archives-ouvertes.fr/hal-00580297

Affiliations:

France

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Sequent calculi and decidability for intuitionistic hybrid logic</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA- UHP Nancy 1, Campus Scientifique, BP239</s1>
<s2>54 506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
<wicri:noRegion>BP239</wicri:noRegion>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Salhi, Yakoub" sort="Salhi, Yakoub" uniqKey="Salhi Y" first="Yakoub" last="Salhi">Yakoub Salhi</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA- UHP Nancy 1, Campus Scientifique, BP239</s1>
<s2>54 506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
<wicri:noRegion>BP239</wicri:noRegion>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">12-0044340</idno>
<date when="2011">2011</date>
<idno type="stanalyst">PASCAL 12-0044340 INIST</idno>
<idno type="RBID">Pascal:12-0044340</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000129</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000882</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000122</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000122</idno>
<idno type="wicri:doubleKey">0890-5401:2011:Galmiche D:sequent:calculi:and</idno>
<idno type="wicri:Area/Main/Merge">002846</idno>
<idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-00580297</idno>
<idno type="url">https://hal.archives-ouvertes.fr/hal-00580297</idno>
<idno type="wicri:Area/Hal/Corpus">004526</idno>
<idno type="wicri:Area/Hal/Curation">004526</idno>
<idno type="wicri:Area/Hal/Checkpoint">002012</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">002012</idno>
<idno type="wicri:doubleKey">0890-5401:2011:Galmiche D:sequent:calculi:and</idno>
<idno type="wicri:Area/Main/Merge">002545</idno>
<idno type="wicri:Area/Main/Curation">002802</idno>
<idno type="wicri:Area/Main/Exploration">002802</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Sequent calculi and decidability for intuitionistic hybrid logic</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA- UHP Nancy 1, Campus Scientifique, BP239</s1>
<s2>54 506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
<wicri:noRegion>BP239</wicri:noRegion>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Salhi, Yakoub" sort="Salhi, Yakoub" uniqKey="Salhi Y" first="Yakoub" last="Salhi">Yakoub Salhi</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA- UHP Nancy 1, Campus Scientifique, BP239</s1>
<s2>54 506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
<wicri:noRegion>BP239</wicri:noRegion>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
<imprint><date when="2011">2011</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Completeness</term>
<term>Computer theory</term>
<term>Constructive theory</term>
<term>Cut elimination</term>
<term>Decidability</term>
<term>Intuitionistic logic</term>
<term>Proof theory</term>
<term>Sequent calculus</term>
<term>Soundness</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Informatique théorique</term>
<term>Décidabilité</term>
<term>Logique intuitionniste</term>
<term>Théorie preuve</term>
<term>Théorie constructive</term>
<term>Calcul séquent</term>
<term>Consistance sémantique</term>
<term>Complétude</term>
<term>Elimination coupure</term>
<term>03B20</term>
<term>03Fxx</term>
<term>68T15</term>
<term>Déduction naturelle</term>
<term>Procédure décision</term>
</keywords>
<keywords scheme="mix" xml:lang="ro"><term>Cut-elimination</term>
<term>Decidability</term>
<term>Intuitionistic hybrid logic</term>
<term>Sequent calculus</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for <sub>IHL</sub>
 and then prove its decidabilit<sup>y</sup>
.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
</list>
<tree><country name="France"><noRegion><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</noRegion>
<name sortKey="Salhi, Yakoub" sort="Salhi, Yakoub" uniqKey="Salhi Y" first="Yakoub" last="Salhi">Yakoub Salhi</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002802 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 002802 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Pascal:12-0044340
   |texte=   Sequent calculi and decidability for intuitionistic hybrid logic
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

Serveur d'exploration sur la recherche en informatique en Lorraine

Sequent calculi and decidability for intuitionistic hybrid logic

Sequent calculi and decidability for intuitionistic hybrid logic

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.